(set-logic QF_UF)
(declare-fun uf3 (Bool) Bool)
(declare-fun uf7 (Bool Bool Bool Bool) Bool)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(assert (= v6 v1))
(push 1)
(assert
 (uf7 true
      (uf7 v3 v5 v4 v5)
      (or v3 (= (not v5) (uf3 v7)))
      (= (not v5) (uf3 v7))
 )
)
(check-sat)
(pop 1)
(check-sat)
